Nuprl Lemma : prod_sum_l_q
11,40
postcript
pdf
a
,
b
:
. (
a
b
)
(
E
:({
a
..
b
}
),
u
:
. (
u
*
a
j
<
b
.
E
(
j
)) =
a
j
<
b
.
u
*
E
(
j
)
)
latex
Definitions
t
T
,
t
.2
,
t
.1
,
CRng
,
<
+*>
,
*
,
x
f
y
,
|
r
|
,
x
:
A
.
B
(
x
)
,
a
j
<
b
.
E
(
j
)
Lemmas
crng
wf
,
qrng
wf
,
rng
times
sum
l
origin
a, b:
. (a 
b) 
(E:({a..b
}
), u:. (u * 
a j < b. E(j)) = a j < b. u * E(j) 
) a, b:. (a b) (E:({a..b}), u:. (u * a j < b. E(j)) = a j < b. u * E(j) ) T+*>x:A. B(x)a j < b. E(j)